the_es:event_system{i:l}, e:es-E(the_es).
(es-isrcv(the_es; e))  (es-sender(the_es; e)  es-E(the_es)) 

latex

Definitions	t  T, Id, x:A. B(x), kind(e), isrcv(k), b, P  Q, sender(e), P  Q, es_info(es), es-kind(es; e), es-sender(es; e), es-E(es), es-isrcv(es; e), x:A  B(x), event_system{i:l}, x:AB(x)
Lemmas	event system wf, sender wf, assert wf, isrcv wf, kind wf, rcv?-kind, Id wf